T:Type, L:T List, P:({x:T| (x  L) }), T':Type, f:({x:T| (x  L) & P(x) }T'), x:T'.
(x  mapfilter(f;P;L))  (y:T. (y  L) & P(y) & x = f(y)) 

latex

Definitions	t  T, x:A. B(x), b, A & B, S  T, S  T, , (x  l), P & Q, x:A. B(x), P  Q, P  Q, P  Q, Prop, ||as||, False, A, AB, , l[i], {T}, SQType(T), mapfilter(f;P;L), filter(P;l), map(f;as)
Lemmas	l member-set, subtype rel list, filter type, map wf, filter wf, nat wf, length wf1, select wf, bool wf, member map filter, assert wf, l member wf, list-subtype